package server.sat;

import java.io.BufferedReader;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.io.PrintWriter;
import java.util.concurrent.Callable;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;

import server.core.Solution;

/**
 * The SATSolverDispatch class defines an object that dispatches a solver
 * for the given CNF data from a {@link SATProblem}, returning a 
 * {@link SATSolution} once it completes.
 * 
 * @author Clayton Edward Taylor
 */
public class SATSolverDispatch implements Callable<Solution> {

	private String problem;

	/**
	 * Creates a new SATSolverDispatch that will dispatch a solver for the
	 * given CNF problem data from the SATProblem.
	 * 
	 * @param problem - The CNF problem data from the SATProblem
	 * @see             SATSolverDispatch
	 */
	SATSolverDispatch(String problem) {

		this.problem = problem;
	}

	/**
	 * Dispatches a solver for the given CNF problem data from a
	 * {@link SATProblem}, returning the solution that it produces as a
	 * {@link SATSolution} object.
	 * 
	 * @return A SATSolution for the given SATProblem
	 * @throws Exception If the solver unexpectedly fails
	 * @see    SATSolverDispatch
	 */
	@Override
	public Solution call() throws Exception {

		String s;
		Process p = null;
		ExecutorService es = Executors.newSingleThreadExecutor();
		try {
			p = Runtime.getRuntime().exec("./glucose_static");
			PrintWriter pw = new PrintWriter(p.getOutputStream());
			pw.write(problem);
			pw.close();
			s = es.submit(new SolutionReader(p.getInputStream())).get();
		} finally {
			if (p != null) {
				p.destroy();
			}
			es.shutdownNow();
		}

		return new SATSolution(s);
	}

	/**
	 * The SolutionReader class defines an implementation of the Callable
	 * interface for String so that the thread executing the <code>call</code>
	 * method can spawn a second thread that blocks waiting for output from
	 * the process (which can only be interrupted by destroying the process).
	 * 
	 * @see SATSolverDispatch
	 */
	private class SolutionReader implements Callable<String> {

		private InputStream is;

		public SolutionReader(InputStream is) {
			
			this.is = is;
		}

		@Override
		public String call() throws Exception {

			InputStreamReader isr = new InputStreamReader(is);
			BufferedReader br = new BufferedReader(isr);

			// Read in only the solution portion of the process output
			StringBuilder sb = new StringBuilder();
			String line;
			while ((line = br.readLine()) != null) {
				line = line.trim();
				if (line.startsWith("s") || line.startsWith("v")) {
					sb.append(line + "\n");
				}
			}
			br.close();

			return sb.toString();
		}
	}
}
